#region Using directives

using System;
using System.Collections.Generic;
using System.Text;

using Weazel.Gezel.Model.Errors;

#endregion

namespace Weazel.Gezel.Model
{
  /// <summary>
  /// Extends the Controller by providing verification 
  /// capabilities.
  /// </summary>
  public partial class Controller : IVerifiable
  {
    /// <summary>
    /// Verifies the controller according to the following rules:
    /// 
    /// Hardwired controllers must have exactly one sfg reference,
    /// Sequential controllers must have a positive number of sfg references,
    /// SignalFlowGraph references must be valid,
    /// Fsm controllers must have an initial state.
    /// </summary>
    /// <param name="errors">the list of verification errors</param>
    /// <param name="arguments">optional custom verification arguments</param>
		public void Verify(ref List<VerificationError> errors, ref List<VerificationWarning> warnings, params object[] arguments)
    {
      sfgs = new Dictionary<string, SignalFlowGraph>();

      // check that the referenced datapath exists
      if (Parent.Datapaths.ContainsKey(datapathRef))
        this.datapath = Parent.Datapaths[datapathRef];
      else
      {
        ErrorMessage message = new ErrorMessage();
        message.AddString("Unknown datapath '" + datapathRef + "' associated with controller '");
        message.AddEntity(this);
        message.AddString("' defined at position ");
        message.AddPosition(StartPosition);
        message.AddString(".");

        errors.Add(new VerificationError(VerificationErrorType.ControllerUnknownDatapath, message));
        return;
      }
     
      if (type == ControllerType.Hardwired)
      {
				verifyHardwired(ref errors, ref warnings);
      }
      // sequential controllers must contain a positive number of sfg references
      else if(type == ControllerType.Sequencer)
      {
				verifySequencer(ref errors, ref warnings);
      }
      else if (type == ControllerType.Fsm)
      {
				verifyFsm(ref errors, ref warnings);
      }

			// verify the name of the controller
			Identifier.Verify(ref errors, ref warnings, LocalName, StartPosition);
    }

    /// <summary>
    /// Verifies a finite-state-machine controller.
    /// Checks for an initial state.
    /// </summary>
    /// <param name="errors"></param>
		private void verifyFsm(ref List<VerificationError> errors, ref List<VerificationWarning> warnings)
    {
      if (initialState == null)
      {
        ErrorMessage message = new ErrorMessage();
        message.AddString("Finite state machine controller '");
        message.AddEntity(this);
        message.AddString("' at position ");
        message.AddPosition(StartPosition);
        message.AddString(" must define an initial state.");

        errors.Add(new VerificationError(VerificationErrorType.ControllerNoInitialState, message));
      }
      else
      {

      }

      if (transitions.Count == 0)
      {
        ErrorMessage message = new ErrorMessage();
        message.AddString("No transitions defined for finite state machine controller '");
        message.AddEntity(this);
        message.AddString("' at ");
        message.AddPosition(StartPosition);
        message.AddString(".");

        errors.Add(
          new VerificationError(
            VerificationErrorType.ControllerFsmNoTransitions,
            message
          )
        );
      }

			// check that each state has a transition associated
			foreach(State state in states.Values)
				if (!transitions.ContainsKey(state.LocalName))
				{
					ErrorMessage message = new ErrorMessage();
					message.AddString("No transitions defined for state '");
					message.AddEntity(state);
					message.AddString("' defined at ");
					message.AddPosition(state.StartPosition);
					message.AddString(".");

					errors.Add(
						new VerificationError(
							VerificationErrorType.ControllerStateNoTransition,
							message
						)
					);
				}

      // check that the referenced sfg's exist 
      foreach (Transition transition in Transitions.Values)
				verifyTransition(ref errors, ref warnings, transition);

    }

		private void verifyTransition(
			ref List<VerificationError> errors, 
			ref List<VerificationWarning> warnings, 
			Transition transition
		)
    {
			verifyFsmCondition(ref errors, ref warnings, transition);

      if (transition.FirstTargetSfgs != null)
        foreach (string sfgReference in transition.FirstTargetSfgs)
					verifySignalFlowGraphReference(
						ref errors, 
						ref warnings, 
						sfgReference, 
						transition.StartPosition,
						transition.EndPosition
					);

      if(transition.SecondTargetSfgs != null)
        foreach (string sfgReference in transition.SecondTargetSfgs)
					verifySignalFlowGraphReference(
						ref errors, 
						ref warnings, 
						sfgReference, 
						transition.StartPosition,
						transition.EndPosition
					);

      // check that the source state has been declared
      if (!this.states.ContainsKey(transition.SourceState))
      {
        ErrorMessage message = new ErrorMessage();
        message.AddString(string.Format("Use of undeclared source state {0} in transtion at ", transition.SourceState));
        message.AddPosition(transition.StartPosition);

        errors.Add(new VerificationError(VerificationErrorType.ControllerUndeclaredSourceState, message));
      }

			// check that the target state exists ..
			if (transition.FirstTargetState != null && !this.states.ContainsKey(transition.FirstTargetState))
			{
				ErrorMessage message = new ErrorMessage();
				message.AddString(string.Format("Use of undeclared target state {0} in transtion at ", transition.FirstTargetState));
				message.AddPosition(transition.StartPosition);

				errors.Add(new VerificationError(VerificationErrorType.ControllerUndeclaredTargetState, message));				
			}

			if (transition.SecondTargetState != null && !this.states.ContainsKey(transition.SecondTargetState))
			{
				ErrorMessage message = new ErrorMessage();
				message.AddString(string.Format("Use of undeclared target state {0} in transtion at ", transition.SecondTargetState));
				message.AddPosition(transition.StartPosition);

				errors.Add(new VerificationError(VerificationErrorType.ControllerUndeclaredTargetState, message));
			}

      if (transition.FirstTransition != null)
				verifyTransition(ref errors, ref warnings, transition.FirstTransition);

      if (transition.SecondTransition != null)
				verifyTransition(ref errors, ref warnings, transition.SecondTransition);
    }

		private void verifyFsmCondition(
			ref List<VerificationError> errors, 
			ref List<VerificationWarning> warnings, 
			Transition transition
		)
    {
      // verify the condition (if it exists)
      if (transition.Condition != null)
      {
				transition.Condition.Verify(ref errors, ref warnings, datapath);

        // check that fsm condition does not reference
        // inports, outports or signals
        List<LeafExpression> leafExpressions = new List<LeafExpression>();
        transition.Condition.GetDependentLeafExpressions(ref leafExpressions);

        foreach (LeafExpression lExpr in leafExpressions)
        {
          if (lExpr.ReferencedEntity is Signal)
          {
            ErrorMessage message = new ErrorMessage();
            message.AddString(
							string.Format("Use of datapath signal {0} in transtion condition at ", 
							(lExpr.ReferencedEntity as Signal).Name)
						);
            message.AddPosition(transition.StartPosition);

            errors.Add(new VerificationError(VerificationErrorType.FsmConditionReferencesSignal, message));
          }
          else if (lExpr.ReferencedEntity is OutPort)
          {
            ErrorMessage message = new ErrorMessage();
            message.AddString(string.Format("Use of datapath outport {0} in transtion condition at ", (lExpr.ReferencedEntity as OutPort).Name));
            message.AddPosition(transition.StartPosition);

            errors.Add(new VerificationError(VerificationErrorType.FsmConditionReferencesOutPort, message));
          }
          else if (lExpr.ReferencedEntity is InPort)
          {
            ErrorMessage message = new ErrorMessage();
            message.AddString(string.Format("Use of datapath inport {0} in transtion condition at ", (lExpr.ReferencedEntity as InPort).Name));
            message.AddPosition(transition.StartPosition);

            errors.Add(new VerificationError(VerificationErrorType.FsmConditionReferencesInPort, message));
          }
        }
      }
    }

		private void verifySequencer(ref List<VerificationError> errors, ref List<VerificationWarning> warnings)
    {
      if (sfgRefs.Count <= 0)
      {
        ErrorMessage message = new ErrorMessage();
        message.AddString("Sequential controller '");
        message.AddEntity(this);
        message.AddString("' defined at position ");
        message.AddPosition(StartPosition);
        message.AddString(" must have atleast one signal flow graph refrence.");

        errors.Add(new VerificationError(VerificationErrorType.ControllerNoSfg, message));
      }

      // check that the referenced sfg's exist      
      foreach (string sfgRef in sfgRefs)
				verifySignalFlowGraphReference(ref errors, ref warnings, sfgRef, startPosition, endPosition);
    }

		private void verifyHardwired(ref List<VerificationError> errors, ref List<VerificationWarning> warnings)
    {
      // if hardwired, only one sfg reference is allowed
      if(sfgRefs.Count != 1) {
        ErrorMessage message = new ErrorMessage();
        message.AddString("Hardwired controller '");
        message.AddEntity(this);
        message.AddString("' at position ");
        message.AddPosition(StartPosition);
        message.AddString(" must have atleast one signal flow graph.");

        errors.Add(new VerificationError(VerificationErrorType.ControllerMultipleSfg, message));
        return;
      }

      // check that the referenced sfg's exist      
      foreach (string sfgRef in sfgRefs)
				verifySignalFlowGraphReference(ref errors, ref warnings, sfgRef, startPosition, endPosition);

      // mark the referenced sfg as driven by hardwired
      // (used for optimization purposes)

      // the sfgref may not be in the collection. This error is caught elsewhere..
      if (datapath.SignalFlowGraphs.ContainsKey(sfgRefs[0]))
      {
        SignalFlowGraph sfg = datapath.SignalFlowGraphs[sfgRefs[0]];
        sfg.IsHardwired = true;
      }      
    }

		private bool verifySignalFlowGraphReference(
			ref List<VerificationError> errors, 
			ref List<VerificationWarning> warnings, 
			string sfgRef,
			Position startPosition,
			Position endPosition
		)
    {
      if (datapath.SignalFlowGraphs.ContainsKey(sfgRef))
      {
        // may already be in the list..
        if(!sfgs.ContainsKey(sfgRef))
          sfgs.Add(sfgRef, datapath.SignalFlowGraphs[sfgRef]);

        return true;
      }
      else
      {
        ErrorMessage message = new ErrorMessage();
        message.AddString("Signal flow graph '" + sfgRef + "' does not exist in datapath '");
        message.AddEntity(datapath);
        message.AddString("' referenced at position ");
        message.AddPosition(StartPosition);
        message.AddString(".");

        errors.Add(new VerificationError(VerificationErrorType.ControllerNoSfg, message));
        return false;
      }
    }
  }
}
